Initial support for RISC-V 32 I M #781

clebreto · 2024-04-08T08:18:16Z

…s (ADD / ADDI). (#706) * Provides RISCV initial architecture description and first instructions (ADD / ADDI). Co-authored-by: Benjamin Gregoire <[email protected]> Co-authored-by: Jean-Christophe Léchenet <[email protected]> --------- Co-authored-by: Benjamin Gregoire <[email protected]> Co-authored-by: Jean-Christophe Léchenet <[email protected]>

Co-authored-by: LE BRETON Come <[email protected]>

Co-authored-by: Santiago Arranz Olmos <[email protected]>

Add XOR and OR to compiler/riscv_instr_decl.v --------- Co-authored-by: Julian Wälde <[email protected]> Co-authored-by: Jean-Christophe Léchenet <[email protected]>

Renames registers. Co-authored-by: Jean-Christophe Léchenet <[email protected]>

Co-authored-by: Jean-Christophe Léchenet <[email protected]>

Riscv compiler skeleton

Co-authored-by: Jean-Christophe Léchenet <[email protected]>

Co-authored-by: Jean-Christophe Léchenet<[email protected]>

Co-authored-by: Jean-Christophe Léchenet <[email protected]>

+ Fix push / pop ra to stack

It looks like gp may be used to access globals. I don't know for tp, but to be safe I added both of them into the list of callee-saved registers.

Co-authored-by: Jean-Christophe Léchenet <[email protected]>

This pass compiles, on RISC-V, complex loads and stores into 3 equivalent instructions for which assembly can be generated. This is kind of a hack for now. Ideally, we would support subarrays with non-constant offset and a way to do pointer arithmetic.

for arm. Proof still required. Co-authored-by: Jean-Christophe Léchenet <[email protected]>

Proof missing in params_core. Co-authored-by: Jean-Christophe Léchenet <[email protected]>

…ctions-in-a-same-fashion-as-it-was-done-for-arm-1 789 risc v test every instructions in a same fashion as it was done for arm 1 Bug fixes to main risc-v branch have been added, as well as compiler pass. It notably adds a lowering compiler pass for complex addresses.

vbgl

Thanks for this hard work. My comments are mostly cosmetic.

vbgl · 2024-09-23T09:10:09Z

compiler/src/help.ml

@@ -17,7 +17,7 @@ let show_intrinsics asmOp fmt =
  let headers = [|
      "no size suffix";
      "one optional size suffix, e.g., “_64”";
-      "a zero/sign extend suffix, e.g., “_u32u16”";
+      "a zero/sign extend suffix, e.g., “_s16” or “_u32u16”";


This is surprising: does it mean that it is now possible to write MOVSX_s16?

Any updates on this issue?

vbgl · 2024-09-23T09:12:35Z

default.nix

+         ppxlib
+         ppx_import
+         ppx_sexp_conv
+         ppx_yojson_conv
+         ppx_deriving
+         sel
+         lsp
+         sexplib


Is this change really meant to be included in this PR?

vbgl · 2024-09-23T09:14:01Z

proofs/compiler/riscv_instr_decl.v

+(*CHECKME*)
+Definition riscv_sra_semi (wn : ty_r) (wm : word U8) : exec ty_r := ok (wsar wn (wunsigned (wand wm (wrepr U8 31)))).
+


Should this be checked before merging?

vbgl · 2024-09-23T09:14:49Z

proofs/compiler/riscv_lower_addressing_proof.v

+(* TODO: move *)
+Lemma write_lval_eq_ex wdb gd X x v s1 s2 vm1 :


This can be addressed before merging.

vbgl · 2024-09-23T09:15:09Z

proofs/compiler/riscv_lower_addressing_proof.v

+(* TODO: move *)
+Lemma sem_sopn_eq_ex X gd o xs es s1 s2 vm1 :


vbgl · 2024-09-23T09:16:31Z

proofs/compiler/riscv_lowering_proof.v

+  riscv_decl
+  riscv_extra
+  riscv_instr_decl
+  (* riscv_instr_decl_lemmas *)


Should this comment be removed?

vbgl · 2024-09-23T09:17:43Z

proofs/compiler/riscv_params.v

+Definition riscv_loparams : lowering_params lowering_options :=
+  {|
+    lop_lower_i _ _ _ := lower_i;
+    lop_fvars_correct := fun _ _ _ => true; (* FIXME RISCV: is this correct? *)


Please fix this.

vbgl · 2024-09-23T09:18:37Z

proofs/compiler/riscv_params_common_proof.v

+(* FIXME try to remove the usage of this lemma, use sem_fopn_args version instead *)
+Lemma align_eval_instr {lp ls ii xname vi y al} {wy : word Uptr} :


Is this really a FIXME? If it is the case, then please fix it. Otherwise please change to TODO.

vbgl · 2024-09-23T09:18:46Z

proofs/compiler/riscv_params_common_proof.v

+(* FIXME try to remove the usage of this lemma, use sem_fopn_args version instead *)
+Lemma sub_eval_instr {lp ls ii xname vi y z} {wy wz : word Uptr} :


vbgl · 2024-09-23T09:19:30Z

proofs/compiler/riscv_params_core_proof.v

+(* Lemma li_lsem_1 s xname vi imm :
+  let: (xi, x) := mkv xname vi in


This comment might be removed.

The passes between stack_alloc and reg_alloc are called twice, first in OCaml and then in Coq. Pass LowerAddressing was inserted between stack_alloc and reg_alloc, but was only called in Coq, creating a discrepancy between the two calls (in OCaml and in Coq). The pass is now called also in OCaml. Due to the way complex Coq types are extracted in OCaml, we had to make some types simpler on the Coq side to be able to call the pass in OCaml.

RA is not used as the return address storage AND the return value in the same function.

RISC-V: automatically introduce registers for constants in conditions This is implemented as a new arch-independent pass called before lowering. A boolean in arch_params controls whether the pass is called (true for RISC-V, false otherwise). Co-authored-by: Jean-Christophe Léchenet <[email protected]>

This reverts commit 7a14e76.

On RISC-V, the return address is read from register RA. This was not reflected in the model and generated wrong programs. The RAstack case of return_address_location is given an additional optional argument ra_return that specifies what register to use (if any) when returning from a function. linearization is adapted to generate the right code. reg alloc and merge_varmaps take into account this potential new register.

Problem : jasmin2ec not working for armm4 or riscv -> x86 used instead in the header.

rtetley and others added 27 commits February 5, 2024 09:14

Add dependencies to build vscoq-language-server (temp fix).

0be66c6

Adds SUB, AND, MV

bfafb60

Co-authored-by: LE BRETON Come <[email protected]>

Adds LOAD and STORE

881bfc8

Co-authored-by: LE BRETON Come <[email protected]>

Refactor cond

121aad6

Co-authored-by: Santiago Arranz Olmos <[email protected]>

Add XOR and OR to compiler/riscv_instr_decl.v (#747)

65371a0

Add XOR and OR to compiler/riscv_instr_decl.v --------- Co-authored-by: Julian Wälde <[email protected]> Co-authored-by: Jean-Christophe Léchenet <[email protected]>

Adds the very minimal bits for dummy compilation.

35faf94

Renames registers. Co-authored-by: Jean-Christophe Léchenet <[email protected]>

WIP : bug-499.

602bee6

Adds li to implement more functionalities.

8055c6d

Co-authored-by: Jean-Christophe Léchenet <[email protected]>

Merge pull request #754 from jasmin-lang/riscv-compiler-skeleton

254fd06

Riscv compiler skeleton

Merge branch 'main' into risc-v

218dc38

Adds XOR lowering.

b0b4453

Co-authored-by: Jean-Christophe Léchenet <[email protected]>

Fix adressing assembly syntax.

3a80c10

Intrepret "subi" as ADDI.

f9fc5db

Factorize instructions by encodings.

9778be6

Co-authored-by: Jean-Christophe Léchenet <[email protected]>

Adds swap and subi as extra ops.

7a00b90

Co-authored-by: Jean-Christophe Léchenet<[email protected]>

Condition lowering implementation.

84b5d1b

Co-authored-by: Jean-Christophe Léchenet <[email protected]>

Provides JAL instruction to match calling convention

12e88bc

Co-authored-by: Jean-Christophe Léchenet <[email protected]>

Provides tests for branching conditions.

9309743

Co-authored-by: Jean-Christophe Léchenet <[email protected]>

Hack to compare with imm.

2f9c8c8

+ Fix push / pop ra to stack

X1 -> X2

ff7977e

X1 -> X2 again

33f5b14

Push and pop ok

50e48b8

assemble_cond: correctly detects 0

6f1cc0e

Fixes program crash

6d84586

It looks like gp may be used to access globals. I don't know for tp, but to be safe I added both of them into the list of callee-saved registers.

Allows to execute at least once each test.

8e2aa91

Merge branch 'main' into risc-v

922c98c

eponier force-pushed the risc-v branch from abaad88 to 922c98c Compare April 10, 2024 09:10

clebreto added 2 commits April 10, 2024 11:35

Check execution of tests.

ff82fa2

Co-authored-by: Jean-Christophe Léchenet <[email protected]>

Adds MUL MULH instructions declaration.

7de90ac

eponier and others added 7 commits September 16, 2024 18:12

Prove riscv_lower_addressing

26fe70b

This pass compiles, on RISC-V, complex loads and stores into 3 equivalent instructions for which assembly can be generated. This is kind of a hack for now. Ideally, we would support subarrays with non-constant offset and a way to do pointer arithmetic.

Fix macos / linux assembly checker option handling

03dab30

Use jasmin shift semantic properly.

11d9268

Introduce smart_addi to stack alloc as done

013919d

for arm. Proof still required. Co-authored-by: Jean-Christophe Léchenet <[email protected]>

Moves subi from ext op to lowering.

a2473d9

Proof missing in params_core. Co-authored-by: Jean-Christophe Léchenet <[email protected]>

End of the proofs

df36861

clebreto marked this pull request as ready for review September 18, 2024 08:03

vbgl reviewed Sep 23, 2024

View reviewed changes

clebreto and others added 9 commits September 30, 2024 16:22

Clear out unused Lemma.

72d4742

FIXME -> TODO.

7212a26

x28 x29 are FP temporaries -> OK

1b6f96f

FIXME -> Comment

2296f15

Fix typo.

9ddd343

Remove comment

9008aad

move write_lval_eq to psem_facts.

eba00c4

Add RA to the list of callee_saved registers.

7a14e76

RA is not used as the return address storage AND the return value in the same function.

clebreto force-pushed the risc-v branch from 86effc3 to 7a14e76 Compare October 8, 2024 12:37

bgregoir and others added 8 commits October 17, 2024 13:53

Merge branch 'main' into risc-v

b74ebeb

adapte 4fc6626 to risc-v

f286134

Merge branch 'main' into risc-v

c1036d6

Revert "Add RA to the list of callee_saved registers."

fd5e550

This reverts commit 7a14e76.

Provides SLT, SLTI, SLTU, SLTIU for RISC-V.

14e0e9a

Provides extraction to EC.

3af7bbd

Problem : jasmin2ec not working for armm4 or riscv -> x86 used instead in the header.

clebreto force-pushed the risc-v branch from 6366293 to 3af7bbd Compare November 16, 2024 09:00

bgregoir added 2 commits November 16, 2024 10:03

Merge branch 'main' into risc-v

f668724

Merge branch 'risc-v' of github.com:jasmin-lang/jasmin into risc-v

984590c

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Initial support for RISC-V 32 I M #781

Initial support for RISC-V 32 I M #781

clebreto commented Apr 8, 2024 •

edited

Loading

vbgl left a comment

vbgl Sep 23, 2024

vbgl Nov 15, 2024

vbgl Sep 23, 2024

vbgl Sep 23, 2024

bgregoir Nov 15, 2024

vbgl Sep 23, 2024

vbgl Sep 23, 2024

vbgl Sep 23, 2024

vbgl Sep 23, 2024

vbgl Sep 23, 2024

vbgl Sep 23, 2024

vbgl Sep 23, 2024

		(CHECKME)
		Definition riscv_sra_semi (wn : ty_r) (wm : word U8) : exec ty_r := ok (wsar wn (wunsigned (wand wm (wrepr U8 31)))).

		(* TODO: move *)
		Lemma write_lval_eq_ex wdb gd X x v s1 s2 vm1 :

		(* TODO: move *)
		Lemma sem_sopn_eq_ex X gd o xs es s1 s2 vm1 :

		(* FIXME try to remove the usage of this lemma, use sem_fopn_args version instead *)
		Lemma align_eval_instr {lp ls ii xname vi y al} {wy : word Uptr} :

		(* FIXME try to remove the usage of this lemma, use sem_fopn_args version instead *)
		Lemma sub_eval_instr {lp ls ii xname vi y z} {wy wz : word Uptr} :

		(* Lemma li_lsem_1 s xname vi imm :
		let: (xi, x) := mkv xname vi in

Initial support for RISC-V 32 I M #781

Are you sure you want to change the base?

Initial support for RISC-V 32 I M #781

Conversation

clebreto commented Apr 8, 2024 • edited Loading

vbgl left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

clebreto commented Apr 8, 2024 •

edited

Loading